Second-order proof systems for algebraic specification languages
Identifieur interne : 001139 ( Istex/Curation ); précédent : 001138; suivant : 001140Second-order proof systems for algebraic specification languages
Auteurs : Pierre-Yves SchobbensSource :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: Besides explicit axioms, an algebraic specification language contains model-theoretic constraints such as term-generation or initiality. For proving properties of specifications and refining them to programs, an axiomatization of these constraints is needed; unfortunately, no effective, sound and complete proof system can be constructed for most algebraic specification languages. In this paper, we construct non-effective second-order axiomatizations for constraints commonly found in specification languages, and simplified forms useful for the universal fragment. They are shown to be sound and complete, but not effective, since the underlying second-order logic is not effective. A good level of machine support is still possible using higher-order proof assistants.
Url:
DOI: 10.1007/3-540-57867-6_20
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: Pour aller vers cette notice dans l'étape Curation :001155
Links to Exploration step
ISTEX:4A574811652078F51413057685A2800B46C4796CCuration
No country items
Pierre-Yves Schobbens<affiliation><mods:affiliation>Institut d'Informatique, Fac. Univ. Notre-Dame de la Paix, Rue Grandgagnage 21, B-5000, Namur</mods:affiliation><wicri:noCountry code="subField">Namur</wicri:noCountry></affiliation>Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Second-order proof systems for algebraic specification languages</title><author><name sortKey="Schobbens, Pierre Yves" sort="Schobbens, Pierre Yves" uniqKey="Schobbens P" first="Pierre-Yves" last="Schobbens">Pierre-Yves Schobbens</name><affiliation><mods:affiliation>Institut d'Informatique, Fac. Univ. Notre-Dame de la Paix, Rue Grandgagnage 21, B-5000, Namur</mods:affiliation><wicri:noCountry code="subField">Namur</wicri:noCountry></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:4A574811652078F51413057685A2800B46C4796C</idno><date when="1994" year="1994">1994</date><idno type="doi">10.1007/3-540-57867-6_20</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-53KFQJJD-9/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">001155</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001155</idno><idno type="wicri:Area/Istex/Curation">001139</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Second-order proof systems for algebraic specification languages</title><author><name sortKey="Schobbens, Pierre Yves" sort="Schobbens, Pierre Yves" uniqKey="Schobbens P" first="Pierre-Yves" last="Schobbens">Pierre-Yves Schobbens</name><affiliation><mods:affiliation>Institut d'Informatique, Fac. Univ. Notre-Dame de la Paix, Rue Grandgagnage 21, B-5000, Namur</mods:affiliation><wicri:noCountry code="subField">Namur</wicri:noCountry></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><title level="s" type="abbrev">Lect Notes Comput Sci</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: Besides explicit axioms, an algebraic specification language contains model-theoretic constraints such as term-generation or initiality. For proving properties of specifications and refining them to programs, an axiomatization of these constraints is needed; unfortunately, no effective, sound and complete proof system can be constructed for most algebraic specification languages. In this paper, we construct non-effective second-order axiomatizations for constraints commonly found in specification languages, and simplified forms useful for the universal fragment. They are shown to be sound and complete, but not effective, since the underlying second-order logic is not effective. A good level of machine support is still possible using higher-order proof assistants.</div></front></TEI></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001139 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Curation/biblio.hfd -nk 001139 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Istex
|étape= Curation
|type= RBID
|clé= ISTEX:4A574811652078F51413057685A2800B46C4796C
|texte= Second-order proof systems for algebraic specification languages
}}
| This area was generated with Dilib version V0.6.33. |  |